;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface Iavltree
  (sig empty-tree ())
  (sig avl-retrieve (tr key))
  (sig avl-insert (tr key datum))
  (sig avl-delete (tr key))
  (sig avl-flatten (tr))
  (sig occurs-in-tree? (k tr))
  (sig tree? (tr)))